Nuprl Lemma : d-single-sframe_wf 0,22
i:Id, L:Knd List, l:IdLnk, tg:Id. @i: only L sends on (l with tg)  Dsys 
latex

DefinitionsDsys, @i: only L sends on (l with tg), if b t else f fi, eqof(d), IdDeq, MsgA, only L sends on (l with tg), x:A. B(x), , IdLnk, Knd, t  T, Id
LemmasId wf, Knd wf, IdLnk wf, ma-empty wf, ma-single-sframe wf, msga wf, id-deq wf, eqof wf, ifthenelse wf

origin